\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$;${\it da}$).
\-\\[0ex]update{-}spec{-}decl(${\it upd}$;${\it ds}$)
\\[0ex]$\Rightarrow$ msg{-}spec{-}loc{-}decl(${\it snd}$;$i$;${\it da}$)
\\[0ex]$\Rightarrow$ $\neg$"ecl" $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ R{-}Feasible(\=ecl{-}machine at $i$ with state ecl\+
\\[0ex]
\\[0ex]$A$
\\[0ex]
\\[0ex]state variables ${\it ds}$
\\[0ex]
\\[0ex]actions ${\it da}$
\\[0ex]
\\[0ex]sends ${\it snd}$
\\[0ex]
\\[0ex]updates ${\it upd}$)
\-\\[0ex]$\Rightarrow$ (\=$\forall$$a$:Id, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type, $T$:Type, $P$:(State(${\it ds}_{2}$)$\rightarrow$$T$$\rightarrow$Prop).\+
\\[0ex]$\neg$"ecl" $\in$ dom(${\it ds}_{2}$)
\\[0ex]$\Rightarrow$ ${\it ds}$ $\parallel$ ${\it ds}_{2}$
\\[0ex]$\Rightarrow$ locl($a$) $\in$ dom(${\it da}$)
\\[0ex]$\Rightarrow$ $T$ $=$ ${\it da}$(locl($a$))
\\[0ex]$\Rightarrow$ \=ecl{-}machine at $i$ with state ecl\+
\\[0ex]
\\[0ex]$A$
\\[0ex]
\\[0ex]state variables ${\it ds}$
\\[0ex]
\\[0ex]actions ${\it da}$
\\[0ex]
\\[0ex]sends ${\it snd}$
\\[0ex]
\\[0ex]updates ${\it upd}$ $\parallel$ @$i$ precondition for $a$(v:$T$):$P$ State(${\it ds}_{2}$) v)
\-\-
\end{tabbing}